/* Benchmarks for the PionterC verifier. */

// null list test

struct list
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @                  (({l}) && list(l->next))
  @ in  list(l)
  @ end
  @*/

int nulltest(struct list* l)
{
  int * p;
  //p = alloc(int);
  if (l==null)
  {
    //free(p);
    return 0;
  }
  else return l->data;
}
/*@ 
  @*/
